5 UPPER AND LOWER INTEGRALS 117 For each integer N g> 1 it follows from (13.5.7) that N N \n=l / n=l N ow apply (12,5.7) to the increasing sequence of partial sums n= 1 If (/n) is any sequence of mappings of X into R, the mapping x h^lim inf /„(*) (resp. x h^lim sup/n(x)) n-*oo n-*oo j defined for all x e X. It is denoted by lim inf/w (resp. lim sup/n). H-+QO «-*oo 13.5,9) (Fatou's lemma) If(fn) is any sequence of functions ^0, then M*(lim inf/.) glim inf /im \ i»-»oo / n-+oo For each n ^ 1, let gn = inf (fn+p). Clearly we have n*(gn] ^ inf ^*(/n+p 1>£0 p^O nd ^n ^0; since the sequence (0rB) is increasing and liminfyj, = sup^nj it ollows from (13.5.7) that ^*/lim inf/n\ = sup v*(gn} ^ sup (inf jU*( \ n-»oo Jn n \p^0 If/: X ~> K is any mapping, we define /**(/) = — /**(-/); this number is ailed the /0vtw integral of /with respect to the measure /i. All the properties .bove which were proved for the upper integral can be immediately translated tito properties of the lower integral. In particular, if we put — J = ^ (or ^(X)), then y is the set of all upper semicontinuous functions on X which are Bounded above by a function belonging to «5TR(X) (which implies that they do lot take the value + oo). For all functions /e £f, we have ind for all/: X -* R we have = sup [1 3.5.10) Iff is any mapping ofX into I, then /**(/) <; /i*(/). otherwise there is